COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	circum.not[f83,jmc]	Notes for circum[f83,jmc]
C00006 ENDMK
C⊗;
circum.not[f83,jmc]	Notes for circum[f83,jmc]

	The result of circumscribing ⊗ab is always a second order
formula because of the quantifier %2∀ab'%1.  However, in the examples
given so far in this paper, the formula is always equivalent to a
first order formula.  Appropriate substitutions for ⊗ab' can be
found to get this formula.  Vladimir Lifschitz (1983) has shown
when ⊗A(P) can be written in prenex form with only universal
quantifiers and no functions, then ⊗A'(P) is always equivalent
to a first order formula.  This result cannot simply be cited
here, because there are functions, namely the aspects.

	However, we can make a heuristic argument (which I hope
will be replaced by a proof) that
what gives trouble is not the functions or existential quantifiers
per se, but rather the possibility of using them to generate
an infinite set of elements satisfying ⊗ab.  This is essentially why the
axiom schema of mathematical induction cannot be reduced to a single formula.
However, iterating the aspect functions does not give anything which
can be proved to satisfy ⊗ab.  

	Even when ⊗A(P) reduces to a first order formula, in general
the formula will involve disjunctions.  This is the case for the
Reiter examples involving Nixon and the city of residence.  However,
in the bird and blocks world examples, we do better.  The first
order formula is obtained by a single substitution for ⊗ab', and
doesn't involve disjunction.

	One might suppose that this would correspond to there being
a unique minimal model, but this doesn't seem to be the case.
It seems rather to be some kind of relative minimal model.  There are
different models with different kinds of birds, but once the interpretations
of the predicates ⊗bird, ⊗ostrich, etc. are fixed, the interpretation
of the variable predicates ⊗ab and ⊗flies are determined uniquely by
circumscribing ⊗ab_z.  One goal in formulating an axiom system
is to achieve unique interpretations of the variable predicates.

	The way we have treated the bird example is a
reformulation in logic of what is often done by
inheritance of properties in ⊗is-a hierarchies.

IT IS NOT PRESENTLY CLEAR WHETHER WE CAN DO EVERYTHING NORMALLY
DONE WITH IS-A HIERARCHIES.

LOGIC AND PSEUDO-LOGIC, STRIPS AND ITS DISCONTENTS.

STANDARDLY NOT USUALLY

CHECK KEITH CLARK WORK AND SEE IF CIRCUMSCRIPTION DOES MORE THAN
PREDICATE COMPLETION.  CHECK HORN CLAUSE CASE.